package com.googlecode.syper.javasyp.checker;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;

import org.eclipse.jdt.core.dom.AST;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.QualifiedName;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.ThisExpression;

import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Name;
import com.googlecode.syper.javasyp.formulae.Ref;

/**
 * Lookup class that allows havoc'ing fields and locals, e.g., when
 * they are re-assigned.
 * @author kevin
 * @since Feb 10, 2010
 *
 */
class EasyHavocLookup extends AbstractHavocLookup<EasyHavocLookup> {

	/** Maps objects to their fields' incarnations (bumped when havoc'ed) */
	private final Map<Name, Map<IVariableBinding, Integer>> fields =
		new HashMap<Name, Map<IVariableBinding, Integer>>();

	/**
	 * Creates a new lookup object; create one for every method
	 * @param ast
	 */
	public EasyHavocLookup(AST ast) {
		super(ast);
	}

	/**
	 * Copy-constructor used for creating a {@link #createClone() clone}
	 * with a shared expression-to-temp map
	 * @param original
	 */
	private EasyHavocLookup(EasyHavocLookup original) {
		super(original);
		for (Map.Entry<Name, Map<IVariableBinding, Integer>> f : original.fields.entrySet()) {
			this.fields.put(f.getKey(), new HashMap<IVariableBinding, Integer>(f.getValue()));
		}
	}

	@Override
	public Field getField(Ref ref, IVariableBinding field) {
		// normalize accessor
		Name access = (Name) ref;
		if (access == null) {
			// FIXME resolution for inner classes
			access = new Local("this", field.getDeclaringClass());
		}

		// normalize field
		if (field != null) {
			if (field.getDeclaringClass() == null && "length".equals(field.getName()))
				field = null;
			else
				field = field.getVariableDeclaration();
		}

		Integer incarnation;
		Map<IVariableBinding, Integer> incarnations = fields.get(access);
		if (incarnations == null) {
			// variable not encoded yet
			incarnations = new HashMap<IVariableBinding, Integer>();
			fields.put(access, incarnations);
			incarnation = 0;
			incarnations.put(field, incarnation);
		}
		else {
			incarnation = incarnations.get(field);
			if (incarnation == null) {
				incarnation = 0;
				incarnations.put(field, incarnation);
			}
		}
		if (field == null) {
			if (incarnation != 0)
				throw new IllegalStateException("array.length was havoc'ed: " + incarnation);
			return new Field(access,
					Local.createFieldVar(Local.ARRAY_LENGTH_FIELD_NAME, intType));
		}
		return new Field(access, incarnation, field);
	}

	@Override
	public Collection<Formula> havoc(
			Map<Name, ? extends Collection<IVariableBinding>> modified) {
		for (Map.Entry<Name, ? extends Collection<IVariableBinding>> mod : modified.entrySet()) {
			Name access = mod.getKey();
			Collection<IVariableBinding> fs = mod.getValue();
			if (! fs.isEmpty()) {
				for (IVariableBinding f : fs)
					havoc(access, f);
			}
		}
		return Collections.emptySet();
	}

	/**
	 * @deprecated Use {@link #havoc(Map)} instead
	 */
	@Deprecated
	public Collection<Formula> havoc(Name access, Collection<IVariableBinding> fs) {
		if (! fs.isEmpty()) {
			for (IVariableBinding f : fs)
				havoc(access, f);
		}
		return Collections.emptySet();
	}

	/** for havoc-ing fields of method parameters */
	private void havoc(Name access, IVariableBinding field) {
		if (field == null)
			return; // don't havoc array length
		Map<IVariableBinding, Integer> incarnations = fields.get(access);
		// nothing to havoc if variable not encoded yet
		if (incarnations != null) {
			Integer incarnation = incarnations.get(field);
			if (incarnation != null)
				incarnations.put(field, incarnation + 1);
		}
	}

	@Override
	public Collection<Formula> havoc(Collection<Expression> es, boolean aroundLoop) {
		if (es.isEmpty())
			return Collections.emptySet();
		List<Formula> result = new LinkedList<Formula>();
		for (Expression e : es) {
			if (e instanceof ArrayAccess)
				result.addAll(havocArrayCell((ArrayAccess) e, aroundLoop));
			else
				havoc(e);
		}
		return result;
	}

	/** for re-assigning variables or fields locally */
	private void havoc(Expression e) {
		if (e instanceof ThisExpression)
			throw new IllegalArgumentException("Cannot havoc " + e);
		IVariableBinding binding;
		if (e instanceof SimpleName) {
			SimpleName var = (SimpleName) e;
			binding = (IVariableBinding) var.resolveBinding();
			if (binding.isEnumConstant()) {
				// do nothing
				return;
			} else if (! binding.isField()) {
				// local (fields below)
				havocLocal(binding);
				return;
			}
		} else if (e instanceof QualifiedName) {
			binding = (IVariableBinding) ((QualifiedName) e).resolveBinding();
		} else if (e instanceof FieldAccess) {
			binding = ((FieldAccess) e).resolveFieldBinding();
		} else if (e instanceof ArrayAccess) {
			throw new IllegalArgumentException("Not handled here: " + e);
		} else
			throw new IllegalArgumentException("Not an lvalue: " + e);
		Field f = (Field) getName(e);
		Map<IVariableBinding, Integer> incarnations = fields.get(f.getObj());
		if (incarnations == null) {
			incarnations = new HashMap<IVariableBinding, Integer>();
			fields.put((Name) f.getObj(), incarnations);
		}
		Integer incarnation = incarnations.get(binding);
		if (incarnation != null)
			incarnations.put(binding, incarnation + 1);
	}

	public Collection<Formula> havocKnownFields(Name n) {
		Map<IVariableBinding, Integer> nFields = fields.get(n);
		if (nFields == null || nFields.isEmpty())
			// nothing to havoc
			return Collections.emptySet();
		for (Entry<IVariableBinding, Integer> field : nFields.entrySet()) {
			if (field.getKey() != null /* skip array.length TODO skip final */)
				// bump incarnation for every known field
				field.setValue(field.getValue() + 1);
		}
		return Collections.emptySet();
	}

	/**
	 * Returns a deep copy of the given lookup that can be used independently
	 * of the receiver (although temps will be shared).
	 * @return Deep copy of the given object except shared temps.
	 */
	@Override
	public EasyHavocLookup createClone() {
		return new EasyHavocLookup(this);
	}

	@Override
	public Collection<Field> getKnownFields(Name n) {
		Map<IVariableBinding, Integer> nFields = fields.get(n);
		if (nFields == null || nFields.isEmpty())
			return Collections.emptyList();
		List<Field> result = new ArrayList<Field>(nFields.size());
		for (IVariableBinding f : nFields.keySet()) {
			// TODO recursively find all transitively reachable fields
			result.add(getField(n, f));
		}
		return result;
	}

	@Override
	protected void mergeLookups(Set<Formula> knowledge,
			EasyHavocLookup other) {
		super.mergeLookups(knowledge, other);

		for (Entry<Name, Map<IVariableBinding, Integer>> obj1 : this.fields.entrySet()) {
			Name var = obj1.getKey();
			Map<IVariableBinding, Integer> fields1 = obj1.getValue();
			Map<IVariableBinding, Integer> fields2 = other.fields.get(var);
			if (fields2 != null) {
				for (Entry<IVariableBinding, Integer> f1 : fields1.entrySet()) {
					IVariableBinding field = f1.getKey();
					Integer i1 = f1.getValue();
					Integer i2 = fields2.get(field);
					if (i2 != null) {
						if (i1 < i2) {
							equate(knowledge, this.getField(var, field), other.getField(var, field));
							f1.setValue(i2);
						} // else nothing to do
					} else {
						fields2.put(field, i1);
					}
				}
			} else {
				// force fields1 onto obj2
				other.fields.put(var, new HashMap<IVariableBinding, Integer>(fields1));
			}
		}
	}
}